/*******************************************************************
 * Author	: Harsh and Maulik
 * Description	: In this file we have tried to implement POBDD and check how many nodes it needs during creation.
 * Last Updated	: 5th Dec, 2011
 *******************************************************************/



#include "BDD.h"

extern int id;
static int tempVar = 1;


void initDecompositionSet(decompositionSet *dSet[])
{
	int i= 0;
        for(;i<20;i++)
                dSet[i] = NULL;

	
}


void showDecompositionSet(decompositionSet *dSet[])
{	
	int i = 0;
	while(dSet[i] != NULL)
	{
		printf("Variable  %s \t Argv %s \n", dSet[i]->variable, dSet[i]->argv );
		i++;
	}

}

decompositionSet * insertDecompositionSet(char *variable,char *argv,vertex *ver)
{
	decompositionSet  *dset = (decompositionSet *) malloc(sizeof(decompositionSet));

	dset->variable = (char *) malloc (sizeof(char) * strlen(variable));
	strcpy(dset->variable,variable);

	dset->argv = (char *) malloc (sizeof(char) * strlen(argv));
	strcpy(dset->argv,argv);
	dset->ver = ver;
}


vertex *buildStepPartial(char *argv, int index, graph *g)
{
	char low[1000] = "\0",high[1000] = "\0";
	char *result = NULL, *temp = NULL, *teq = NULL,*negate = NULL;
	char * pch;
	char delims[] = "+";
	char tempName[1000] = "temp";
	char tempName1[2];
	vertex* tempVertex;
	int itr,flag=0;


// This is for POBDD setup
	if(index > 2)
	{
		itr = 0;
		flag=0;
		printf(" Decomposition on way!\n");
		tempName1[0] = '0'+ tempVar;
		tempName1[1] = '\0';
		while((g->dSet[itr]) != NULL)
		{
			if(strcmp(g->dSet[itr]->argv,argv) == 0)
			{
				flag=1;
				break;
			}
			itr++;
		}
		if(flag == 1)
		{
			tempVertex = g->dSet[itr]->ver;
		} else 
		{
			tempVertex  = insertVertex(3,((g->totVar)+tempVar),strcat(tempName,tempName1),id);
                        g->dSet[tempVar-1] = insertDecompositionSet(tempName,argv,tempVertex);
                        tempVar++;
                        id++;
		}
		return tempVertex;
	}
//	Argv is the equation.

	result = (char *)strtok( argv, delims );
	int number;
	int value;

	tempVertex = insertVertex(3,(index+1),g->variables[index],id);
	id++;


	while(result != NULL)
	{


		pch = (char *) strstr(result,g->variables[index]);

		while( condition(pch, result, g->variables[index],'.'))
		{
			pch++;
			pch = (char *) strstr(pch,g->variables[index]);
		}

		if (pch == NULL)
		{  
			strcat(low,result);
			strcat(high,result);
			
		} else {

			
			if(result[pch-result-1] == '~') {
				temp = result;
				strcat(high,"0");
				
				negate = (char *) malloc (sizeof(g->variables[index])+1);
				negate[0] = '~';
				negate[1] = '\0';
				
				strcat(negate,g->variables[index]);
				teq = expression(temp,negate);
				strcat(low,teq);
				free(negate);



			} else {

				temp = result;
				strcat(low,"0");
	
				teq = expression(temp,g->variables[index]);
				strcat(high,teq);


			}

		}
		result = (char *)strtok( NULL, delims );


		if(result != NULL)
		{
			if(strlen(low) != 0)
				strcat(low,"+");
			if(strlen(high) != 0)
				strcat(high,"+");
		}


	}





	printf("Low equation is  :%s \n", low);

	pch = (char *) strstr(low,"1");
	while( condition(pch, low, "1",'+'))
        {
                        pch++;
                        pch = (char *) strstr(pch,"1");
        }



	if (pch != NULL )
		strcpy(low,"1");
	else
		strcpy(low,refine(low));
	printf("Refined low equation is  :%s \n", low);



	printf("High equation is :%s \n", high);

	pch = (char *) strstr(high,"1");
        while( condition(pch, high, g->variables[index],'+'))
        {
                        pch++;
                        pch = (char *) strstr(pch,"1");
        }

	if (pch != NULL )
		strcpy(high,"1");
	else
		strcpy(high,refine(high));

	printf("Refined high equation is :%s \n", high);

	index++;

	value = atoi(low);

	
	if( low[0] == '1' || low[0] == '0' )
	{   
		 tempVertex->low = insertVertex(value,((g->totVar)+1),"\0",id);
		id++;
	} else {
		tempVertex->low = buildStepPartial(low, index, g);		
	}

	value = atoi(high);
	
	if( high[0] == '1' || high[0] == '0' )
	{	//Create Terminal vertex high
		tempVertex->high = insertVertex(value,((g->totVar)+1),"\0",id);
		id++;
	} else {
		tempVertex->high = buildStepPartial(high, index, g);	
	}

	return tempVertex;
	
}


void copyIndex(graph *g, vertex *v,int var)
{

	int i =0;
        v->mark = !(v->mark);

       while(g->variables[i] != NULL)
        {
                if(strcmp(g->variables[i],v->c) == 0)
		{
			v->index = i+1;
			break;
		}
                i++;
        }

	if(v->low != NULL)
	{
		if((v->low->value == 0) || v->low->value == 1)
		{	
			v->low->index = (g->totVar)+1;
		}
 	}

	if(v->high != NULL)
	{
		if((v->high->value == 0) || (v->high->value == 1))
        	{
                	v->high->index = (g->totVar)+1;
	        } 
	}



        if((v->index) <= (var-1) )                   
        {
                if((v->mark) != (v->low->mark))
                        copyIndex(g,v->low,var);

                if ((v->mark) != (v->high->mark))
                        copyIndex(g,v->high,var);

        }


        return ;

}

void copyVertex(vertex *newVertex, vertex *oldVertex, graph *gTemp, graph *g)
{
	newVertex->low = oldVertex->low;
        newVertex->high = oldVertex->high;
        strcpy(newVertex->c,oldVertex->c);
        newVertex->value = oldVertex->value;
        newVertex->id = oldVertex->id;
        newVertex->mark = oldVertex->mark;
	copyIndex(g,newVertex,g->totVar);
	
}




void buildPartial(graph *g,char * argv)
{
	int i = 0,newNode = id;
	graph gTemp;
	tempVar = 1;
	initDecompositionSet(g->dSet);
	g->root = buildStepPartial(argv, 0,g);
	showDecompositionSet(g->dSet);

	while(g->dSet[i] != NULL)
	{
		initVariables(g->dSet[i]->argv, gTemp.variables, &gTemp);
		build(&gTemp,g->dSet[i]->argv);
		reduction(&gTemp,(gTemp.totVar)+1);
		copyVertex(g->dSet[i]->ver, gTemp.root,&gTemp,g);
		i++;
		free(gTemp.root);
	}
	reduction(g,((g->totVar)+1));	
	printf("Total Node needed for POBDD = %d\n", id-newNode);
}
